$\forall$${\it da}$:$z$:Knd fp$\rightarrow$ Type. Kind(${\it da}$) $\in$ Type